the_es:ES, e:E, l:IdLnk. rcvs(l;before(e))  {e:E| haslnk(l;e) } List 

latex

Definitions	pred(e), before(e), as @ bs, haslnk(l;e), rcvs(l;before(e')), Unit, P  Q, P & Q, first(e), , b, b, IdLnk, ij, ES, SWellFounded(R(x;y)), x:A. B(x), Prop, (e <loc e'), T, True, A, False, AB, , E, P  Q, x:A. B(x), t  T
Lemmas	es-E wf, le wf, es-locl wf, nat wf, es-locl-swellfnd, event system wf, nat properties, IdLnk wf, assert wf, not wf, bnot wf, bool wf, es-first wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, es-haslnk wf, append wf, es-pred wf, es-pred-locl, es-before wf, filter append